0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 784 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 5 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 601 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 90 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPSizeChangeProof (⇔, 0 ms)
↳43 YES
↳44 PiDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 PiDP
↳47 PiDPToQDPProof (⇒, 0 ms)
↳48 QDP
↳49 QDPSizeChangeProof (⇔, 0 ms)
↳50 YES
↳51 PiDP
↳52 UsableRulesProof (⇔, 0 ms)
↳53 PiDP
↳54 PiDPToQDPProof (⇒, 0 ms)
↳55 QDP
↳56 QDPSizeChangeProof (⇔, 0 ms)
↳57 YES
↳58 PiDP
↳59 UsableRulesProof (⇔, 0 ms)
↳60 PiDP
↳61 PiDPToQDPProof (⇒, 0 ms)
↳62 QDP
↳63 QDPSizeChangeProof (⇔, 0 ms)
↳64 YES
↳65 PiDP
↳66 UsableRulesProof (⇔, 0 ms)
↳67 PiDP
↳68 PiDPToQDPProof (⇒, 0 ms)
↳69 QDP
↳70 QDPSizeChangeProof (⇔, 0 ms)
↳71 YES
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
TIMESK_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, multI_in_gga(T28, T29, T31))
TIMESK_IN_GGA(s(T28), T29, T31) → MULTI_IN_GGA(T28, T29, T31)
MULTI_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, multA_in_ga(T51, T54))
MULTI_IN_GGA(s(T51), 0, T54) → MULTA_IN_GA(T51, T54)
MULTA_IN_GA(s(T63), T65) → U1_GA(T63, T65, multA_in_ga(T63, T65))
MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)
MULTI_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, multB_in_ga(T99, T102))
MULTI_IN_GGA(s(T99), s(0), s(T102)) → MULTB_IN_GA(T99, T102)
MULTB_IN_GA(s(T119), s(T121)) → U2_GA(T119, T121, multB_in_ga(T119, T121))
MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U11_GGA(T155, T158, multC_in_ga(T155, T158))
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTC_IN_GA(T155, T158)
MULTC_IN_GA(s(T183), s(s(T185))) → U3_GA(T183, T185, multC_in_ga(T183, T185))
MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_GGA(T219, T222, multD_in_ga(T219, T222))
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTD_IN_GA(T219, T222)
MULTD_IN_GA(s(T255), s(s(s(T257)))) → U4_GA(T255, T257, multD_in_ga(T255, T257))
MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_GGA(T291, T294, multE_in_ga(T291, T294))
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTE_IN_GA(T291, T294)
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → U5_GA(T335, T337, multE_in_ga(T335, T337))
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_GGA(T371, T374, multF_in_ga(T371, T374))
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTF_IN_GA(T371, T374)
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U6_GA(T423, T425, multF_in_ga(T423, T425))
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_GGA(T459, T462, multG_in_ga(T459, T462))
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTG_IN_GA(T459, T462)
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U7_GA(T519, T521, multG_in_ga(T519, T521))
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_GGA(T555, T558, multH_in_ga(T555, T558))
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTH_IN_GA(T555, T558)
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_GA(T623, T625, multH_in_ga(T623, T625))
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_GGA(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → U18_GGGA(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → U19_GGGA(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
TIMESK_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, multI_in_gga(T28, T29, T31))
TIMESK_IN_GGA(s(T28), T29, T31) → MULTI_IN_GGA(T28, T29, T31)
MULTI_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, multA_in_ga(T51, T54))
MULTI_IN_GGA(s(T51), 0, T54) → MULTA_IN_GA(T51, T54)
MULTA_IN_GA(s(T63), T65) → U1_GA(T63, T65, multA_in_ga(T63, T65))
MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)
MULTI_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, multB_in_ga(T99, T102))
MULTI_IN_GGA(s(T99), s(0), s(T102)) → MULTB_IN_GA(T99, T102)
MULTB_IN_GA(s(T119), s(T121)) → U2_GA(T119, T121, multB_in_ga(T119, T121))
MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U11_GGA(T155, T158, multC_in_ga(T155, T158))
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTC_IN_GA(T155, T158)
MULTC_IN_GA(s(T183), s(s(T185))) → U3_GA(T183, T185, multC_in_ga(T183, T185))
MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_GGA(T219, T222, multD_in_ga(T219, T222))
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTD_IN_GA(T219, T222)
MULTD_IN_GA(s(T255), s(s(s(T257)))) → U4_GA(T255, T257, multD_in_ga(T255, T257))
MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_GGA(T291, T294, multE_in_ga(T291, T294))
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTE_IN_GA(T291, T294)
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → U5_GA(T335, T337, multE_in_ga(T335, T337))
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_GGA(T371, T374, multF_in_ga(T371, T374))
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTF_IN_GA(T371, T374)
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U6_GA(T423, T425, multF_in_ga(T423, T425))
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_GGA(T459, T462, multG_in_ga(T459, T462))
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTG_IN_GA(T459, T462)
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U7_GA(T519, T521, multG_in_ga(T519, T521))
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_GGA(T555, T558, multH_in_ga(T555, T558))
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTH_IN_GA(T555, T558)
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_GA(T623, T625, multH_in_ga(T623, T625))
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_GGA(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → U18_GGGA(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → U19_GGGA(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)
MULTH_IN_GA(s(T623)) → MULTH_IN_GA(T623)
From the DPs we obtained the following set of size-change graphs:
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)
MULTG_IN_GA(s(T519)) → MULTG_IN_GA(T519)
From the DPs we obtained the following set of size-change graphs:
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)
MULTF_IN_GA(s(T423)) → MULTF_IN_GA(T423)
From the DPs we obtained the following set of size-change graphs:
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)
MULTE_IN_GA(s(T335)) → MULTE_IN_GA(T335)
From the DPs we obtained the following set of size-change graphs:
MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)
MULTD_IN_GA(s(T255)) → MULTD_IN_GA(T255)
From the DPs we obtained the following set of size-change graphs:
MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)
MULTC_IN_GA(s(T183)) → MULTC_IN_GA(T183)
From the DPs we obtained the following set of size-change graphs:
MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)
MULTB_IN_GA(s(T119)) → MULTB_IN_GA(T119)
From the DPs we obtained the following set of size-change graphs:
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637)
MULTJ_IN_GGGA(s(T662), T663, 0) → MULTI_IN_GGA(T662, s(T663))
MULTJ_IN_GGGA(T676, T677, s(T678)) → MULTJ_IN_GGGA(T676, T677, T678)
From the DPs we obtained the following set of size-change graphs:
MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)
timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)
MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)
MULTA_IN_GA(s(T63)) → MULTA_IN_GA(T63)
From the DPs we obtained the following set of size-change graphs: